\documentclass[orivec]{llncs}

\usepackage{headers}
\usepackage{macro2}
\usepackage{xspace}
\usepackage[noend]{algpseudocode}
\usepackage{algorithm}


%opening

\title{Activity Networks with Delays}

\author{%
  Cinzia Di Giusto\inst{1} \and
  Jean-Louis Giavitto\inst{2} \and
  Hanna Klaudel\inst{1} \and
  Antoine Spicher\inst{3} 
}

\institute{%%
  IBISC, Université d'Evry - Val d'Essonne, Evry, France %
  \and %
  CNRS, IRCAM, UPMC - UMR 9912 STMS \& INRIA MuTAnt team, Paris, France 
  % 
  \and %
  LACL, Université Paris-Est, Créteil, France}


\begin{document}
\widowpenalty=0
\clubpenalty=0

\maketitle 
\vspace{-0.75cm}
\begin{abstract}
      \andy, Activity Networks with Delays, is a discrete time framework
      aimed to the qualitative modeling of time-dependent activities such as biological signaling networks and regulatory pathways. 
%      
      Activities involve entities playing the role of
      activators, inhibitors or results. They may have given durations, \ie the time required to obtain results. 
      An entity  may represent an object (\eg
      an agent, a biochemical species or a family of thereof) with a
      local attribute denoting  its level (\eg concentration, strength). Entities levels may change as a result of an activity  or may diminish gradually as time passes by. 
    %  
      The semantics of \andy is formally given via  high-level Petri nets.
      As main results we show that \andy systems have finite state representations even for potentially infinite processes and that  \andy's concept of time has a direct counterpart in timed automata. 
      These results together with a modular and concise syntax  make \andy suitable for an easy and natural modeling of  time-dependent (biological) systems. 
\end{abstract}
 
\vspace{-0.95cm}
\section{Introduction}

Activities are a central concern in many domains such as business (workflows, supply chains), transaction modeling (database transactions, web services) or biological systems (signaling networks, regulatory pathways).
%, to mention some. 
These activity-driven domains, although quite different, share foundational principles that concern, in general, two dimensions:  control-flow  and control-data factors.  Control-flow  refers to the causal relationships
 among activities, how long does it take to complete them, when they can be performed,  %, if they must be executed with time progression 
 or whether they can be delayed or even ignored. 
Control-data, instead,  addresses how data can play a role in promoting or  preventing an activity.\looseness=-1

Our main motivation comes from biological systems where data are species and activities the reactions among them. 
Our proposal stems from reaction systems %as defined in 
\cite{DBLP:journals/ijfcs/BrijderEMR11}, a formalism based on  \emph{reactions},
each defined as a triple $(R, I, P)$ with $R$  set of
\emph{reactants}, $I$  set of \emph{inhibitors} and $P$  set of
\emph{products}, and $R,I$ and $P$  taken from a common set of
\emph{species}. Reaction systems are based on three foundational
principles:
%\begin{enumerate}[1.]
% \item \label{item:react} 
(i) a reaction can take place only if all the reactants involved are available but none of the inhibitors are; 
 %\item \label{item:quantity} 
(ii) if a species is available then a sufficient amount of it is present to trigger a reaction; 
% \item 
(iii) species are not persistent: they become unavailable if they are not sustained by a reaction.
%\end{enumerate}
%
We complement this model by adding features to both control-flow and control-data dimensions. On the one side, each species is better characterized by an attribute that may specify its expression degree, rate of presence, etc. %\footnote{A first attempt in this direction is \cite{CDGHKFD14}.}.  
On the other side, the main difference with respect to reaction systems lies in  the introduction of time aspects.  
More precisely, the resulting formalism, \emph{Activity Networks with Delays} (\andy), 
targets systems 
composed of various \emph{entities} (\ie species in reaction systems) that evolve by means of time-dependent activities.
Each entity is characterized by one attribute,
called \emph{level}, representing rates, thresholds of activation/inhibition or expression degrees
(\eg low, medium, high). 
\emph{Activities} are rules describing the evolution of systems, involving (as for reaction systems) three sets of entities:
\emph{activators}, which must be present, 
\emph{inhibitors}, which must be absent,  
and \emph{results} whose expression levels have to be modified (increased or decreased).
The introduction of time concerns both activities and entities. Activities have a duration and entities are subject
to a \emph{decay} process or aging that models the action of a
non-specified environment: levels decrease with time
progression.
Another difference is in the semantics of activities: while in reaction systems a maximal concurrency model is considered, here we  
adopt two types of activities:  \emph{mandatory} and \emph{potential} ones. The former set of activities, once enabled, must take place altogether in the same time unit (in maximal concurrency) while the latter, non deterministically one at the time, may be performed or not.  
Following \cite{Wang04formalverification}, as in our modeling all entities share the same global clock, it is reasonable to work with discrete time constraints.\looseness=-1 


 Our main objective is to provide effective tools for the
 description and  the understanding of the mechanisms and of the
 structural properties underpinning biological interactions networks. In
 biology, ordinary differential equations (ODE) remain the
 predominant modeling methodology. Such models present however some
 drawbacks:
random interactions are difficult to model outside an averaged
 approach, %
 system openness and non-linearities make hopeless the existence of
 analytic solutions, %
 and numerical methods -- often the only sensible option -- are mainly
 descriptive and cannot form the basis for an explanatory theory. 
 On the other hand, many
 languages and tools  have been developed  to build and explore discrete qualitative
 models in various application domains. Such models are rough
 abstractions of real world processes but they make possible to unravel
 the entangled causal relationships between system's entities.
 %%
 More specifically in systems biology, formalisms like Petri
 nets~\cite{DBLP:journals/nc/BaldanCMS10}, boolean networks~\cite{thomas1973boolean},
 process algebras~\cite{journals/tcsb/Cardelli05} 
or rewriting
 systems~\cite{giavitto04a} (to cite a few) have been used with
 undeniable success to understand the causal links between structure
 and behavior in molecular networks.
  Nonetheless, the management of time is somewhat problematic in all of
 the previous examples. In general, time aspects are either disregarded or they are handled with stochastic or continuous methodologies. This is why here we propose  a qualitative discrete model for biological systems that explicitly takes into account time aspects such as activity duration and decay. 



%\paragraph
\noindent{\bf Organization of the paper.} 
%The paper is organized as follows: 
%%
Section \ref{sec:reaction} introduces the principles behind \andy
networks
and gives a formal definition of \andy in terms of high-level Petri nets. It also states the main results of the paper  addressing the finiteness of state space and the expressiveness of the formalism in terms of timed automata.
%%
 %This translation assess the handling
%of \andy's temporal concepts in a  well known framework.
The encoding of an \andy network into timed automata is exponential 
showing the expressive relevance and the concision of the original
\andy's notation.
%%
Finally Sections \ref{sec:related} and \ref{sec:concl} discuss related works and conclude.
%with some perspectives opened by the first simulation and model-checking
%tools developed for \andy.
An Appendix with  additional details 
%of the encoding into timed automata 
is added for the reviewer convenience.\looseness=-1


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Activity Networks with Delays}\label{sec:reaction}

In this section we give the syntax and   
semantics of \emph{Activity Networks with Delays} (\andy) which is composed of a set of entities
\entities governed by a set of activities.\looseness=-1 

%\paragraph
\noindent{\bf Entities.} 
Entities  represent the actors of the modeled
system. %They may be concrete objects or more abstract concepts such as the state of an object. 
%%
Each entity, $\entity \in \entities$, is associated to a finite number of levels $\setlev_{\entity}$ (from 0 to $\setlev_{\entity}-1$), that 
in general represent ordered expression degrees (\eg low, medium,
high) and refer to a change in the entity capability of action.
Levels have a decay duration which
is either $\omega$ (unbounded) or a  natural number $\life_\entity:[0 \mydots \setlev_\entity-1] \to \nat^+ \cup \{\omega \}$
allowing
different durations for different levels. We fix $\life_{\entity}(0) = \omega$ as no negative level is allowed. 
%The intuition behind decay duration is that i
If $\life_\entity(i) =
\omega$, then level $i$ is \emph{permanent} and it can be modified
only by an activity. Otherwise, if $\life_\entity(i) \neq \omega$, the presence of the entity
at level $i$ is \emph{transient}: it decays or ages gradually
% (\eg decrease or increase the level)  THIS GOES IN THE CONCLUSIONS
as time passes by. In principle, this substitutes a set of unspecified activities accounting for the action of an underspecified   
environment that consumes entities.  
A state $\state$ of an \andy network assigns to each entity $\entity \in \entities$ a level $\eta \in [0..\setlev_{\entity}-1]$. The initial state $\state_0$ sets each entity $\entity$ to a given level $\level{\entity}$. 
 

%\paragraph
\noindent{\bf Activities.}
The evolution of entities is governed by \emph{activities} 
%$\rho$ of the form
%\begin{equation}\label{eq:reaction}
 $     \rho ::= \activ{A_{\rho}}{I_{\rho}}{\dur{\rho}}{R_{\rho}}$,  
%\end{equation}
where $\dur{\rho} \in \nat$ is the activity duration, $A_{\rho}$ (activators) and $I_{\rho}$
(inhibitors) are sets of pairs $(\entity, \level{\entity})$, and $R_{\rho}$
(results) is a non empty set of pairs $(\entity, v)$, with $\entity\in
\entities$, $\level{\entity} \in [0 \mydots \setlev_\entity-1]$ and $v \in
\mathbb{Z}$. 
Entities can appear at most once in each set $A_{\rho}$, $I_{\rho}$ and $R_{\rho}$. 
We write $e \in A_{\rho}$ to denote  $(e, \cdot) \in A_{\rho}$, similarly for $I_{\rho}$ and $R_{\rho}$. We omit index $\rho$ if it is clear from the context.

An activity $\rho$  can be executed only if it is \emph{enabled}, this depends on
 the activator and inhibitor
thresholds appearing in  $A_{\rho}$ and $I_{\rho}$. Nonetheless, observing only the current level of each entity is not enough to
decide if an activity is enabled: such approach will miss the handling
of decays and durations. 
%%
To take into account a notion of elapsed time, an activity $\rho$ is
enabled (\ie may happen) if and only if:
\begin{itemize}
 \item for each entity $\entity_a$ of the activators set $A_{\rho}$ (\ie $(\entity_a, \level{a}) \in A_{\rho}$), $\entity_a$ is available at least at level $\level{a}$ for
  the whole duration $\dur{\rho}$;
 \item for each entity $\entity_i$ of the inhibitors set $I_{\rho}$ (\ie $(\entity_i, \level{i}) \in I_{\rho}$), $\entity_i$ is available at a level strictly inferior to $\level{i}$ for
  the whole duration $\dur{\rho}$;
\end{itemize}
Activator and inhibitor thresholds are \emph{inclusive}: if an
      entity is an activator (resp. an inhibitor) at level
      $\ell$ for some activity $\rho$, it is also an activator (resp. an
      inhibitor) for $\rho$ at all levels $l \ge \ell$ (resp. $l \le \ell$).
When an activity is executed, entities' levels appearing in
the results are updated with the increment or decrement (modulo the range of entity levels) $v$ specified in the rule. Duration $\dur{\rho}$ characterizes the time required for yielding change of
levels of results, $\dur{\rho} =0 $ denotes an instantaneous activity.
%%


\begin{remark}
Notice that:
\begin{itemize}
 \item       An
      entity may be both in $A$ and $R$, \eg as in an
      auto-catalytic production where reaction products themselves are activators for the reaction. Similarly, an
      entity may be both in $I$ and $R$: thus representing activities that can be perfomed just once.
      
 \item 
Activators and inhibitors are not ``consumed''.

      
\item An entity can appear in the same activity simultaneously as an
      activator and an inhibitor but we require them to
      occur with different levels. For instance, the rule
      $$
      \activ{\{({\entity},\level{})\} \cup A}{\{({\entity}, \level{}')\} \cup I}{\dur{}}{R}
      \qquad  \text{where~}   \level{} < \level{}'
      $$
      requires that the activity takes place only if the level
      $\lev_{\entity}$ of ${\entity}$ belongs to the interval $\level{}
      \leq \lev_{\entity} < \level{}'$. In particular, if ${\entity}$
      has to be present in an activity exactly at level $\level{}$,
      ${\entity}$ should appear as an activator at level $\level{}$ and
      as inhibitor at level $\level{}' = \level{}+1$.

      
\item The set of activators and inhibitors $A \cup I $ is allowed to be
      empty. In this case, the activity is constantly enabled. This
      accounts for modeling an environment that  continuously
      sustains the production of an entity. In this case a duration
      $\dur{} \not= 0$ may be used to account for a start-up time.

\item Once triggered an activity $\rho$ must wait at least $\dur{\rho}$ before being enabled again\footnote{This is a non restrictive hypothesis and by slightly modifying Definition \ref{def:rs} one can obtain different semantics that could depend on the specific modeled scenario: \eg once enabled an activity $\rho$ can be triggered an unbounded number of times or  once per time unit.}.
      
\end{itemize}
%%
 
\end{remark}



%\paragraph{\Obligatory and \potential activities.}
% It is important to note that when an activity is enabled, it is not
% necessarily performed. The idea is to make a distinction between

Activities are of two types: 
\begin{enumerate}
\item \emph{\obligatory} activities, denoted $\beta$ in a set $\Syn$: if
      enabled  they \emph{must} occur within the same time unit. All enabled
      \obligatory activities occur simultaneously.

\item \emph{\potential} activities, denoted $\alpha$ in a set $\Reac$:
      if enabled, they \emph{may} occur in an interleaved way thus the result
      depends on the order they are performed;

\end{enumerate}


%
It may happen that several \obligatory activities $\beta_i$ referring
to the same entity $\entity$ in their results are triggered
simultaneously. In this case, all updates related to $\entity$ are
collected and summed up before being applied to the current level of
$\entity$. 

Summing up, an \emph{\andy network} is a triple $(\entities, \Syn, \Reac)$ where
$\entities$ is the set of entities, $\Syn$ is the set of \obligatory
activities and $\Reac$ is the set of \potential ones. It evolves by triggering enabled activities in two separate phases:
\begin{enumerate}[Ph. 1]

\item \label{item:reaction} %%
      In this phase \textbf{\potential activities} that are
      enabled may be triggered. Their action occurs in an interleaved
      way. Any potential activity is triggered at most once in this phase
      and the time does not progress. 


\item \label{item:clock} %%
      This phase is the time transition: a time unit passes by during which all  concerned entities must decay and  all enabled \textbf{\obligatory
        activities} are performed simultaneously.
      %% 
      Notice that as activators and inhibitors are not consumed, there
      are no conflicts and so there is a unique way (per time unit) to
      execute all enabled \obligatory activities.
\end{enumerate}



\begin{example}[Repressilator]\label{ex:rep}
The repressilator \cite{Elowitz} is a synthetic genetic regulatory
network in Escherichia Coli consisting of three genes ($lacI, tetR, cI$) connected in a feedback loop, such
that each gene inhibits the next gene and is inhibited by the previous
one. The repressilator exhibits a stable oscillation with fixed time
period that is witnessed by the synthesis of a green fluorescent protein ($GFP$).
%%
According to \cite{Elowitz}: \emph{``the resulting oscillation with typical periods of hours are slower than the cell division cycle so the state of the oscillator has to be transmitted from generation to generation''}.  

It may be modeled with five entities $\entities =\{lacI, tetR, cI, GFP, gen\}$.
The first three represent the three genes,  each with two levels denoting an \emph{on}/\emph{off} state where level
$1=on$ has decay time $2$. $GFP$ has two levels (\emph{on}/\emph{off}) with unbounded decay. 
Finally, the evolution of successive generations is represented by entity $gen$ with seven levels (with unbounded decay) to differentiate among generations.  
 
The behavior is modeled  with \potential and \obligatory activities: the first set (on the left below) is used to represent the feedback loop between $lacI, tetR, cI$. The second set (on the right) handles the synthesis of $GFP$ and shows the evolution of generations.
%
\[
\begin{array}{ll}
 \alpha_1: \activ{\emptyset}{(lacI,1)}{2}{(tetR,+1)} \quad  &  \beta_1: \activ{(lacI,1)}{\emptyset}{0}{(GFP, +1)}  \\
 \alpha_2: \activ{\emptyset}{(tetR,1)}{2}{(cI,+1)} &  \beta_2: \activ{(lacI,0)}{(lacI,1)}{0}{(GFP,-1)}\\
 \alpha_3: \activ{\emptyset}{(cI,1)}{2}{(lacI,+1)} &  \beta_3: \activ{(gen,0)}{(gen, 6)}{1}{(gen, +1)}\\
 &  \beta_4: \activ{(gen,6)}{\emptyset}{1}{(gen, -6)} 
\end{array}
\]
%
We now exhibit a possible execution scenario for the repressilator, the table below shows for each line the current level of each entity:
\[
\begin{tabular}{c|c|c|c|c|l}
 ~$lacI$~ & ~$tetR$~ & ~$cI$~ & ~$GFP$~ & $gen$ & ~description\\
   0    &  0     &    1 &   0   &   0   & ~initial state\\
   0    &  0     &    1 &   0   &   1   &  ~after Ph. 2 x 2 (activity $\beta_3$) \\
   0    &  1     &   1  &   0   &   1   & ~after Ph. 1 (activity $\alpha_1$)\\
   0    &  1     &   0  &   0   &   2   & ~after Ph. 2 x 2 (decay of $cI$ + activity $\beta_3$)\\
   1    &  1     &   0  &   0   &   2   & ~after Ph. 1 (activity $\alpha_3$)\\    
   1    &  0     &   0  &   1   &   3   & ~after Ph. 2 x 2 (decay of $tetR$ + activities $\beta_1$, $\beta_3$)
\end{tabular}
\]

Appendix \ref{app:repressilator} has some additional material on this example. 
Moreover,  a second more detailed example  with an execution scenario that can help getting the handle on the formalism can be found in Appendix \ref{ex:battery}.
\hfill $\diamond$
\end{example}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\subsection{\bf Petri Net formalization.}\label{sec:petri} 

The semantics of \andy networks is formalized in terms of high-level Petri nets. 
%
%We first formalize the notion of state of a
%network and then we specify the behavior of the network as the
%evolution of a high-level Petri net.
%In our approach, the model of time of an \andy network is managed
%explicitly in the functioning of the Petri net. 
%and not as the time
%evolution of the Petri net itself. This approach is relevant but makes
%uneasy to assess the temporal properties of the \andy framework because
%two \andy networks will give raise to two different Petri nets.
%% Cinzia: FALSE!
%%
%For this reason, we have developed an equivalent semantics in terms of
%timed automata. This semantics is presented in the next section.
We recall here their general notations together with some elements of their
semantics  \cite{DBLP:series/eatcs/Jensen92}.

\begin{definition}\label{def:PTS} 
A {\bf high-level Petri net}  is a tuple $(P, T, F, L, M_0)$ where:
\begin{itemize}
 \item $P$ is the set of places, $T$ is the set of transitions, with $P \cap T = \emptyset$;

 \item $F \subseteq (P \times T) \cup (T \times P)$ is the set of arcs; 
 \item $L$ is the labeling  of $P \cup T\cup F$%places $P$, transitions $T$ and arcs $F$   to  a set of labels 
defined as follows:
\renewcommand{\labelitemii}{$-$} 
\begin{itemize}
 \item $\forall p \in P$, $L(p) $ is a set of values;% the type of $p$;%, \ie a (possibly infinite) set or Cartesian product of sets of integer values;
 \item $\forall t \in T$, $L(t)$ is a  computable boolean expression (a guard);%  with variables and integer values; 
 \item and $\forall f\in F$, $L(f)$  is a  tuple of variables or values.% compatible with the adjacent place.  
\end{itemize}
 \item $M_0$ is the initial marking putting a multiset of tokens in $L(p)$ in each   $p \in P$.\looseness=-1
\end{itemize} 
\end{definition}
Observe that we are considering a subclass of high-level Petri nets where at most one arc per direction  for each pair place/transition   is allowed and only one token can flow through. 
The behavior of high-level Petri nets is defined as usual: markings are functions from places in $P$ to multisets of possibly structured tokens in $L(p)$ and a transition $t \in T$ is \emph{enabled} at  marking $M$, if there exists a valuation $\sigma$ of all variables in the labeling of $t$  such that the guard $L(t)$ evaluates to true ($L_{\sigma}(t) = \mathsf{true}$) and there are enough tokens in all input places $p$ to satisfy the corresponding input arcs, \ie $L_{\sigma}((p,t)) \in M(p)$.
% and all input arc labels are $ \qquad \forall q \in \pre{t},   [L((q,t))]_{\sigma} \in M(q),$$
%where $\pre{t} =\{q\in Q \mid (q,t) \in F\}$ denotes the set of input places of a transition $t$. 
The firing of $t$ produces the marking $M'$:  
$\forall p \in P, M'(p) = M(p) - L_{\sigma}((p,t)) + L_{\sigma}((t,p))$
with $L_{\sigma}(f) = 0 $ if $f\notin F$, $-$ and $ +$ are  multiset  operators for removal and adding of one element, respectively. We denote it by $\firing{M}{t}{\sigma}{M'}$. 

As usual, in figures, places are represented as rounds, transitions as squares, 
and arcs as directed arrows.
By convention, primed version of variables (\eg $x'$) are used to annotate 
output arcs of transitions, their evaluation is  
possibly computed using unprimed 
variables (\eg $x$) appearing on input arcs. 
With an abuse of notation, singleton markings are denoted without brackets, 
the same is used in  arc annotations. 
Also we refer to valuated variables without effectively mentioning the valuation $\sigma$: \eg we say that the current value of variable $w$ is $w$ instead of $\sigma(w)$.
An example of firing is shown in  
Appendix \ref{app:exfiring}. 
We say that a marking $M$ is \emph{reachable} from the initial marking 
$M_0$ if there exists a firing sequence $(t_1, \sigma_1), \mydots, (t_n, \sigma_n)$ such that 
 $\firing{M_0}{t_1}{\sigma_1}{M_1} \mydots \firing{M_{n-1}}{t_n}{\sigma_n}{M}$.


\paragraph{\bf \andy's formalization.} We observe that time is strictly linked to entity levels: \ie in order to properly describe decay and the semantics of activities we need to record three kinds of information:
\begin{enumerate}
 \item (decay) since how long an entity is at the current level, starting from the last update,
 \item (activators) since how long an entity is available at a level less or equal to the current one (recall that levels are inclusive),  
 \item (inhibitors) since how long a level greater than the current one has been left.
\end{enumerate}
Notice that durations relative to Items 1 and 2 for the current level can be different: \ie  if an entity is continuously sustained
by some activities it remains available in the system at the current
level for a period that may be longer than the corresponding decay
time. Thus  Item 1 reports the duration since the \emph{last} update (\ie when the activity concerning the entity has been performed) and Item 2 is the duration since the \emph{first} appearance of the entity at that level.

For this reason, we model each entity $\entity \in \entities$ by a single Petri net place $p_{\entity}$ carrying  tuples
$\tuple{\bool_\entity, \refr_\entity, \birth_\entity}$ as tokens where
%%
$\bool_\entity$ is  the current level of $\entity$; 
%%
$\refr_\entity$ is a counter storing the duration spent in the current level since the last update (Item 1): $0 \leq \refr_\entity \leq \life_\entity(\bool_\entity)$; 
%%
and $\birth_\entity$ is a tuple of counters with $\setlev_\entity$ fields (one for
each level).  Each counter $\birth_{\entity}[i]$ contains a
duration interpreted as follows:
$$
\birth_{\entity}[i] = 
\begin{cases}
\begin{minipage}{6.5cm}
  since how long $\entity$ has reached level  $i$ (Item 2)
\end{minipage}
 &  \text{for }  0 \leq i \leq \lev_{\entity}\\
\\
\begin{minipage}{6.5cm}
   since how long $\entity$ has left level $i$ (Item 3)\\(or $0$ if $\entity$ has not yet reached $i$).
\end{minipage} 
& \text{for } \lev_{\entity} < i \leq \setlev_{\entity}-1              
\end{cases}
$$

Each place is initialized to $\tuple{\level{\entity}, 0,
  0^{\setlev_\entity} }$ where $\level{\entity}$ is the given initial
level of $\entity$ and $0^{\setlev_\entity}$ denotes vector $\birth_\entity$ of counters
uniformly initialized with zero.
 
It is worth observing that once a duration in $\birth$ has reached the maximum duration for all activities ($D = \max\{\Delta_\rho \mid \rho \in \Syn \cup \Reac \}$) it is useless to increment it, as for all durations greater than $D$, the guard of all activities involving the entity is satisfied.  


\begin{newnotation}
      We denote
      by $\birth\sub{x}{[l \mydots l + n ]}$ the systematic update of
      values in counters $\birth[l] \mydots \birth[l+n]$ to $x$. 
      $\inc{D}{\birth}$ is the increment by one of all values in $\birth$:
      \ie $\forall k \in [0 \mydots \setlev_\entity-1]$, $\birth[k] =
      \min(\birth[k]+1, D)$ with $D \in \nat$.
\end{newnotation}

In order to cope with time aspects present in \andy, we introduce a tick transition $t_c$ (Figure \ref{fig:clock}) that represents the time progression.  Its effect is the one described by Phase Ph. \ref{item:clock} above: it increments  counters of entities,  takes care of the decay and simultaneously performs all enabled \obligatory activities. More precisely: % updates due to time progression  are performed as follows:
      \begin{description}
      \item [Time: ] All counters in the entities are incremented by
            one: we pass from $\tuple{\lev, \refr, \birth}$ to
            $\tuple{\lev, \refr+1, \inc{D}{\birth}}$.  %We assume that
            Counter $\refr$ remains unchanged for levels of unbounded
            duration.
      \item [Decay: ] An entity may stay at level $\lev$ for
            $\life(\lev)$ time units (\ie $\refr \leq \life(\lev)$).
            Decay happens as soon as the interval $\life(\lev)$ is
            elapsed and is obtained by decreasing the level by one, till
            reaching level zero.  %More formally, 
            We pass from
            $\tuple{\lev, \refr, \birth}$ to $\tuple{\lev - 1, 0,
              \inc{D}{\birth}\sub{0}{\lev}}$.

      \end{description}

Updates on a place $p_r$ of a result entity $r$ at level $\lev_r$ containing token  $\tuple{\lev_r, \refr_r, \birth_r}$, due to an activity $\rho$ (\ie $(r,\pm n) \in R_{\rho}$ with $n\in \nat$) 
are performed\footnote{For the sake of simplicity, in the explanation we consider updates that do not exceed allowed boundaries, these cases are handled as expected in Definition \ref{def:rs}.} as follows : 
\begin{description}
 \item[Increase $+n$:]  
   $\tuple{\lev_r + n, 0, \birth_r\sub{0}{[\lev_r + 1\mydots \lev_r + n]}}$.
  $\lev_r$ becomes $\lev_r +n$, $\refr_r$ is reset to 0 restarting the counter  for level $\lev_r +n$ and 
$\birth_r$ is updated to record the change to the new level by resetting the counters $\birth_r[i]$ for all levels $i$ from $\lev_r + 1$ to $\lev_r + n$.
 
 \item[Maintenance $0$:]  $\tuple{\lev_r, 0, \birth_r}$: the current level is recharged resetting $\refr_r$ to 0.

  \item[Decrease $-n$:]  
	    $\tuple{\lev_r - n, 0, \birth_r\sub{0}{[\lev_r-n+1 \mydots \lev_r] }}$. This case is symmetric to the increase one, except for the treatment of $\birth_r$ that is updated by resetting  counters   $\birth_r[i]$
for all levels $i$  from  $\lev_r - n + 1$ to $\lev_r$.
\end{description}
%%
%%
% Once performed, the next execution of the same activity is possible after at least $\dur{\rho}$ time units.






Finally, every \potential activity $\alpha \in \Reac$ is modeled with  a transition $t_{\alpha}$ (Figure \ref{fig:reaction})  %with a special place $p_{\alpha}$ that  ensures that the same activity is not executed more than once every $\dur{\alpha}$ time units, 
complying to Phase Ph. \ref{item:reaction} above.







%\subsection{\bf Petri net modeling of \andy}


\begin{figure}[t]
\centering
\subfigure[Clock transition. \label{fig:clock}]{
\begin{tikzpicture}[node distance=1.5cm,>=stealth',bend angle=20,auto]

  \node [place, label = right: $p_{\rho}$, label = above: $\vdots$,label = below: $\vdots$] at (3.5,0) (Pc){};
  \node [place, label=left:$p_{\entity}$,label = above: $\vdots$,label = below: $\vdots$]at (0,0)  (R){};

  \node [transition] (tC) at (2,0) {$t_{c}$}
   edge [pre,bend left]    node[above] {$w_{\rho}$}    (Pc)
   edge [post,bend right]   node[below]{$w'_{\rho}$}    (Pc)
   edge [pre,bend right]    node[above] {${\scriptstyle \tuple{\bool_{\entity},\refr_{\entity},\birth_{\entity}}}$}    (R)
   edge [post,bend left]    node[auto] {${\scriptstyle \tuple{\bool_{\entity}',\refr_{\entity}',\birth_{\entity}'}}$}    (R);
  
\end{tikzpicture}
} \quad
\subfigure[Transition for $\alpha\in\Reac$. \label{fig:reaction}]{
\begin{tikzpicture}[node distance=1.5cm,>=stealth',bend angle=20,auto]

 \node [place, label = right: $p_r$,label = left: $\cdots$] at (0,-1.5) (P){};
 %\node [place, label = above: $\Pclock$] at (0,2) (Pc){};
 \node [place, label = below: $p_a$,label = above: $\vdots$] at (-2,0) (R){};
 \node [place, label = below: $p_i$,label = above: $\vdots$] at (2,0) (I){};
 \node [place, label = right: $p_{\alpha}$] at (0,1.5) (qw){};
 
 \node [transition] at (0,0) (tr) {$t_{\alpha}$}
  % edge [pre and post]    node[above] {$z$}    (Pc)
   edge [pre and post]    node[above] {${\scriptstyle \tuple{\bool_{\entity},\refr_{\entity},\birth_{\entity}}}$}   (R)
   edge [pre and post]    node[above] {${\scriptstyle \tuple{\bool_{\entity},\refr_{\entity},\birth_{\entity}}}$}     (I)
   edge [pre, bend right]    node[left] {${\scriptstyle \tuple{\bool_r,\refr_r,\birth_r}}$}   (P)
   edge [post, bend left]   node[right] {${\scriptstyle \tuple{\lev'_r,\refr'_r,\birth_r'}}$}     (P)
   edge [pre, bend left]    node[left] {$w_{\alpha}$}   (qw)
   edge [post, bend right]   node[right] {$w'_{\alpha}$}     (qw);
   
  
\end{tikzpicture}
}
\caption{Scheme of Petri net modeling of \andy.}
\end{figure}



\begin{definition}\label{def:rs}
 Given an  \andy network $(\entities, \Syn, \Reac)$ with initial 
state $(\entity, \level{\entity})$ for each $\entity \in \entities$, 
%Let $D = \max\{\dur{\alpha} \mid \alpha \in \Syn \cup \Reac\}$. 
the high-level Petri net representation is defined as 
tuple $(P, T, F, L, M_0)$ where  $\lev$, $\lev'$, $\refr$, $\refr'$, $\birth$, 
$\birth'$, $w$, $w'$ range over variables and:
\begin{itemize} 
 \item $P = \{p_\entity \mid  \entity\in{\entities}\} \cup \{p_{\rho} \mid  \rho \in \Syn \cup \Reac \}; $
 \item $T= \{t_c \} \cup \{t_{\alpha} \mid \alpha \in \Reac \}$;

 \item $F= \{(p,t_c),(t_c, p) \mid p \in P \} \quad  \cup$ \\
 \hspace*{0.63cm} $ \{ (p_\entity,t_{\alpha}),(t_{\alpha}, p_\entity), (p_{\alpha},t_{\alpha}),
		(t_{\alpha}, p_{\alpha}) \mid \alpha \in \Reac, 
		\entity \in A_{\alpha} \cup I_{\alpha} \cup R_{\alpha} \}$

 \item Labels for places in $P$: 
\[
\begin{array}{lr}
  L(p_{\rho})  = [0 \mydots D] & \text{ for each } \rho \in \Syn \cup \Reac  \\
L(p_\entity) = [0\mydots\setlev_\entity-1] \times [0 \mydots d] \times  [0 \mydots D]^{\setlev_\entity}  
& \text{ for each } \entity\in\entities 
\end{array}
\]
with $d = \max\{\life_{\entity}(i)\mid i \in [0 \mydots \setlev_\entity-1]\}$ and $D = \max\{\dur{\rho}\mid \rho \in \Syn \cup \Reac\}$
\item Labels for arcs in $F$:
\[
\begin{array}{llr}
 L((p_{\rho}, t_c)) = w_{\rho} & L((t_c, p_{\rho} )) = w'_{\rho} & \text{ for each } \rho \in \Syn \cup \Reac\\
    L((p_\entity, t_c)) = \tuple{\bool_\entity, \refr_\entity, \birth_\entity} 
		& L((t_c, p_\entity)) = \tuple{\bool_\entity', \refr_\entity', \birth_\entity'} 
		& \text{ for each } \entity\in\entities
\end{array}
\]
For each \potential activity $\alpha\in\Reac$ and $\entity \in A_{\alpha} \cup I_{\alpha} \cup R_{\alpha}$:
\[
\begin{array}{llr}
      L((p_\entity, t_{\alpha})) = \tuple{\bool_\entity, \refr_\entity, \birth_\entity} \quad 
		& L((t_{\alpha}, p_\entity)) = \begin{cases}
                           \tuple{\bool_\entity, \refr_\entity, \birth_\entity} & \text{if } \entity\notin R_{\alpha}\\
                           \tuple{\bool_\entity', \refr_\entity', \birth_\entity'} & \text{otherwise}
                          \end{cases}\\

     L((p_{\alpha}, t_{\alpha})) = w_{\alpha} & L((t_{\alpha}, p_{\alpha} )) = w'_{\alpha}
\end{array}
\]

\input{algorithm}

% \begin{figure}[t]
% \[
% \begin{array}{l}
% \text{Algorithm } \mathit{Calc}\\
% \quad \text{\bf for each } \rho \in \Syn \cup \Reac \text{ {\bf do} } w_{\rho}'=\max(w_{\rho}+1,D)\\
% %\text{endfor}\\
% 
% \quad\text{\bf for each } \entity\in\entities \text{ {\bf do}}\\
% \quad\qquad \lev_\entity'=\lev_\entity 
% \quad\qquad \refr_\entity'=\refr_\entity
% \quad\qquad \birth_\entity'=\inc{D}{\birth_\entity}\\
% \quad\qquad
% \begin{array}{@{}lll}
% \text{{\bf if }} & \life(\lev_\entity) \neq \omega &\text{  {\bf then} } \quad \refr_\entity'= \refr_\entity + 1\\
% \text{{\bf if }} & \refr_\entity > \life(\lev_\entity) &\text{  {\bf then} } \quad \lev_\entity'= \max(0, \lev_\entity -1) \quad\quad  \refr_\entity'= 0
% \end{array}\\
% %\text{endfor}\\
% 
% \quad\text{{\bf for each} } \beta \in \Syn \text{ {\bf do}}\\
% \quad\qquad \text{{\bf if} } \bigwedge_{(a, \level{a}) \in A_{\beta}}(\lev_a \geq \level{a} \wedge  \birth[\level{a}] \geq \dur{\beta} )  \quad \wedge\\
% \quad\qquad \quad \bigwedge_{(i, \level{i}) \in I_{\beta}}(\lev_i < \level{i} \wedge \birth[\level{i}] \geq \dur{\beta} )  \quad \wedge 
%  \quad\quad (w_{\beta} \geq \dur{\beta}  )\\
% \quad\qquad\text{{\bf then} }
%  \quad\qquad \qquad w'_{\beta} = 0\\
%  \quad\qquad \qquad \text{{\bf for each} } (r,v)\in R_{\beta} \text{ {\bf do}} \\
%  \quad\qquad \qquad \qquad \lev_r'= \lev_r' +v \qquad \refr_r'= 0\\
% %\qquad \qquad \text{endfor} \\
% %\qquad \text{endif}\\
% 
% \quad\text{{\bf for each} } \entity \in \entities \text{ {\bf do}}\\ %Est-ce bien ça ? no c'etait un typo
% \quad\qquad \lev_r'= \max(0, \min(\lev_r', \setlev_r-1 ) \\
% \quad\qquad \text{{\bf case} } \lev_\entity' - \lev_\entity \text{ {\bf of}}\\
% \quad\qquad \qquad [\lev_\entity' - \lev_\entity<0]:  \birth_\entity'=\birth'_\entity\sub{0}{[\lev_\entity'+1\mydots \lev_\entity]}\\
% \quad\qquad \qquad [\lev_\entity' - \lev_\entity>0]:  \birth_\entity'=\birth_\entity'\sub{0}{[ \lev_\entity+1 \mydots \lev_\entity']}\\
% %\qquad \text{endcase}\\
% 
% 
% %\text{endfor}\\
% \quad\text{{\bf return} } \bigwedge_j x'_j=c_j \\
% \end{array}
% \]
% where $x_j'$ is the variable labeling  an output arc of $t_c$ and $c_j$ is its evaluation via $\mathit{Calc}$ 
% 
% \caption{$\mathit{Calc}$ algorithm} \label{fig:calc}
% \end{figure}



\item Labels for transitions in $T$:
 \[
 L(t_c) = \mathit{Calc}
 \]
where $\mathit{Calc}$ is given by Algorithm \ref{fig:calc} whose input is part of the unique valuation $\sigma$ for net variables of input arcs of $t_c$ coming from the current marking,  and which returns the conjunction of equalities of the form $x_j' = c_j$ for each net variable $x_j'$ labeling an output arc  of $t_c$ such that   $\sigma(x_j')=c_j$.
 
\[
\begin{array}{lcl}
L(t_{\alpha}) \! &=&  w_{\alpha} \geq \dur{\alpha}  \wedge  w'_{\alpha} = 0 \quad \wedge \\
&& \bigwedge_{(a, \level{a}) \in A_{\alpha}}(\lev_a \geq \level{a} \wedge \birth[\level{a}] \geq \dur{\alpha} )  \quad \wedge\\
&&  \bigwedge_{(i, \level{i}) \in I_{\alpha}}(\lev_i < \level{i} \wedge \birth[\level{i}] \geq \dur{\alpha} )  \quad  \wedge \\


&& \bigwedge_{(r,+n) \in R_{\alpha}} C_{r+} \wedge \bigwedge_{(r,0) \in E_{\alpha}}C_{r0} \wedge  \bigwedge_{(r,-n) \in R_{\alpha}}C_{r-},\\  
\end{array}
\]
for each \potential activity $\alpha\in\Reac$ with
\[
\begin{array}{ll}
C_{r+} \!&:\!  \tuple{\lev'_r, \refr'_r, \birth'_r} = \tuple{\min(\lev_r +n, \setlev_r-1), 0, \birth_r\sub{0}{[\lev_r +1 \mydots \min(\lev_r +n, \setlev_r-1 ]}} \\
C_{r0} \!&: \! \tuple{\lev'_r, \refr'_r, \birth'_r} = \tuple{\lev_r, 0, \birth_r} \\

C_{r-} \!&: \! \tuple{\lev'_r, \refr'_r, \birth'_r} = \tuple{\max(0,\lev_r-n), 0, \birth_r\sub{0}{[\min(0,\lev_r-n) \mydots \lev_r]}}.
\end{array}
\]

 

\item The initial marking is $M_0(p_{\entity})= \tuple{\level{s},0,0^{\setlev_\entity}}$ for each  $\entity\in \entities$ and $M_0(p_{\rho})= 0$ for 
$\rho\in \Syn \cup \Reac$.
% , the initial marking $M_0$ is:
% \[
% M_0(p) =
% \begin{cases}
%  0 & \text{if } p = p_{\rho} \\
%  \tuple{\level{s},0,0^{\setlev_\entity}}& \text{if } p = p_\entity
% \end{cases}
% \]
\end{itemize}
\end{definition}



We now comment on the transitions guards. 
Input and output arcs between the same place and transition with the same label (read arcs) are denoted in figures with a double-pointed arrow with a single label.
 We detail the conditions and the results of firing of $t_{\alpha}$ corresponding to a \potential activity $\alpha= \activ{A}{I}{\dur{}}{R}$. We have:
\begin{itemize}
 \item each activator $a \in A$ has to be present at least at  level $\level{a}$ for at least $\dur{}$ time units, this is expressed by  guard $\lev_a \geq \level{a} \wedge \birth[\level{a}] \geq \dur{} $; 
 \item each inhibitor $i\in I$ has not to exceed  level $\level{i}$ for at least $\dur{}$ time units,  this is guaranteed by guard 
$\lev_i < \level{i} \wedge \birth[\level{i}] \geq \dur{}$;
\item each result is updated according to conditions $C_{r+}$ (increase), $C_{r0}$ (maintenance), $C_{r-}$ (decrease);
\item place $p_{\alpha}$ retains whether the activity can be performed $w_{\alpha}\geq\dur{}$.

%
%if a result $r \in R $ has to be increased maintained or decreased then the corresponding place $p_r$ is updated to:
%\begin{description}
 %\item [increase:] $\tuple{\min(\lev_r +n, \setlev_r-1), 0, \birth_r\sub{0}{[\lev_r +1 .. \min(\lev_r +n, \setlev_r-1 ]}}$
 %\item [maintenance:] $ \tuple{\lev'_r, \refr'_r, \birth'_r} = \tuple{\lev_r, 0, \birth_r} $
 %\item [decrease:] $ \tuple{\lev'_r, \refr'_r, \birth'_r} = \tuple{\max(0,\lev_r-n), 0, \birth_r\sub{0}{[\min(0,\lev_r-n).. \lev_r]}}$. 
%\end{description}
\end{itemize}
Transition $t_c$ is always enabled, the effect of the firing is that  all connected places are modified according to the valuation $\sigma$ ``computed'' by algorithm $\mathit{Calc}$. The firing updates the levels of all entities dependently if they are involved in a \obligatory activity or decay and increments the counters in $p_{\rho}$ ($w'_{\rho} = w_{\rho}+1$) for all $\rho \in \Syn \cup \Reac$ unless a \obligatory activity $\beta$ is performed in which case the corresponding $w'_{\beta}$ is set to 0.\looseness =-1





\paragraph{\bf Expressiveness.}
The first result that we show for \andy networks concerns the finiteness of the state space. 
On the one hand finiteness is guaranteed by the fact that the number of levels is finite, on the other hand the finiteness of temporal aspects depends on a subtler observation.
In principle a discrete time system should have an infinite state space (accounting for the infinite evolution of time). Nonetheless in our case, when the local counters have reached the maximal duration for activities $D$, no new behaviors can be triggered by the system. This immediately provides a way of abstracting without loosing precision and thus getting a symbolic representation. %:  a kind of quotient of the infinite state space. \looseness=-1

\begin{theorem}
 Let $N$ be an \andy network. The state space of $N$ is finite
\end{theorem}
\begin{proof}[Sketch]
 The proof follows  from the observation that the type of tokens for each place is finite and each place can have at most one token. \qed
\end{proof}

In order to better understand and support the notion of time for \andy we appeal to  timed
automata \cite{DBLP:journals/tcs/AlurD94}. Since their introduction 
they have been widely used to
model complex real time systems and to check their temporal
properties.
Appendix \ref{sec:timedauto} shows the complete encoding and gives some intuitions on the proof of the theorem. Here we report only the main result  that the semantics in terms of timed
automata is equivalent to the one of Definition \ref{def:rs}.

\begin{theorem}
\andy can be encoded into timed automata preserving the semantics. The size of the encoding is exponential.
\end{theorem}

This last result not only clarifies that \andy can suitably handle time aspects but also it underlines the concision of the model. 
As a matter of fact, the syntax of \andy profits from the advantages of Petri net modeling: \ie the state space is the combination of local information.  This is  not the case for automata where the number of localities is already exponential.
Moreover the rule-based architecture of \andy guarantees a modular construction of systems which is not the case neither (in general) for Petri nets nor for timed automata. 
     


\section{Related works}\label{sec:related}

From a technical point of view, the closest related work is on reaction
systems \cite{DBLP:journals/ijfcs/BrijderEMR11} or their Petri net
representation \cite{koutnyreaction}. Although we use a similar
definition for activity, the semantics we have proposed is inherently
different: in \cite{DBLP:journals/ijfcs/BrijderEMR11} all enabled
reactions occur in one step while we consider two forms of activity evolution: simultaneous  for \obligatory activities and
interleaved for \potential ones.
%%
Furthermore, we have introduced discrete abstract  levels that, to the
best of our knowledge, are not taken into account in reaction systems. 
Also, we have presented a more elaborated notion of time that governs
both entities and activities. 
%%
In  \cite{DBLP:conf/birthday/BrijderER11} the authors consider an
extension of reaction systems with duration but it concerns only decay
and not  duration of activities. Furthermore the decay is  referred to
the number of steps and not to the discrete time progression as in our case.\looseness=-1  

From the Petri net modeling point of view, our representation of time is considerably different from the approaches traditionally used in time and timed Petri nets 
(\cite{DBLP:journals/tcs/CeroneM99} presents a survey with insightful
comparison of the different approaches).
%%
The main difference lies on the fact that the  progression of time is implicit and  external to the system. By contrast, in our proposal we have assumed the presence of  an explicit way of incrementing durations (modeled by synchronized counters). 
This is also  different from the notion of timestamps introduced in  \cite{timestamp} that again refers to an implicit notion of time.
Indeed,  our approach is conceptually closer to Petri nets with causal time  \cite{DBLP:journals/entcs/ThanhKP02} for the presence of an explicit transition for time progression. Nevertheless, in our approach time cannot be suspended under the influence of the environment (as is the case in \cite{DBLP:journals/entcs/ThanhKP02}).\looseness=-1
%%
 
In a broader sense, our work could also be related to P-systems
\cite{DBLP:journals/ijfcs/PaunPRS11,DBLP:journals/fuin/KleijnK11} or the
$\kappa$-calculus \cite{DBLP:journals/tcs/DanosL04} that  describe the
evolution of cells through rules. 
%%
Both these approaches are mainly oriented to simulation while we are
interested in  verification aspects. Finally, always related to the
modeling in Petri nets but with a different aim, levels have been used
in qualitative approaches to address problems related to the
identification of steady states in genetic networks such as in
\cite{DBLP:journals/nc/ChaouiyaNRT11}. 
%Similarly in workflow modeling, several models have been proposed \cite{DBLP:conf/dfg/EshuisW03}.
Nevertheless these contributions
abstract away from time related aspects that are instead central in our
proposal.  
Finally, it is interesting to notice that our formalisms adds a new node in between timed and qualitative regions in the classification in   \cite{DBLP:conf/apn/HeinerG11}.



 
 
\section{Final remarks}\label{sec:concl}


We have introduced \andy %, a high-level Petri net framework
to model
time-dependent activity-driven systems. Systems consist of a set of entities
present in the environment at a given level. Entities can age as time
passes by and their level is governed by a set of \obligatory and \potential activities with duration. 
The resulting Petri net is compact and provides an intelligible
graphical representation of the described activities. Moreover, the
network is easily scalable: the size of the network grows linearly with
the number of added entities and activities. 
%In an activity, entities can have the role of activators, inhibitors and
%results. 
%An activity has a given duration. 
 %and it can take place only if
%all activators are available and all inhibitors are not for the whole
%duration of the activity. Depending on the type of activity, results
%levels are either increased, maintained or decreased. 
We have shown that, despite the ability of modeling timed (thus infinite) systems,  \andy networks have finite state space and that they have an alternative but exponential formulation with  equivalent semantics into timed automata. 

As the semantics of \andy is given in terms of high-level Petri nets, \andy networks can be easily used as overlay of existing implemented tools.
%
%
%The main application of our work concerns the verification of properties
%of systems defined in terms of  activities. 
We have prototyped a
tool to simulate and build the state space of an \andy network 
%relying on the high-level Petri net semantics and 
using the SNAKES
toolkit~\cite{Pom-PNN-2008}. We
have also developed an alternative implementation using the MGS
framework~\cite{giavitto2008} to test several strategies that can be
used to avoid the combinatorial explosion and to build lazily the state
space. 
The first results are very positive,  \andy is particularly suited to describe biological systems, in particular regulatory networks and pathways whose formalization is based on rules (activities). 
The tools above have been effectively used in the analysis of several
applications: in physiology (modeling the metabolism of glucose)  \cite{CDGHKFD14}, in the
modeling of regulatory networks (\eg the repressilator),
etc. %The results will be reported elsewhere.
We also plan to use  the design and simulation tool Snoopy \cite{DBLP:conf/apn/HeinerHLRS12} and related analysis tool MARCIE \cite{DBLP:conf/apn/HeinerRS13}. 

%
 We plan to develop the \andy
approach along several directions. We want to extend decay function to arbitrary maps in $\setlev$. The
problem is to generalize the notion of increase and decrease in a
relevant way for the application. More structure can also be given to
the notion of entity. Characterizing an entity by several attributes
(instead of only one level) raises the question of the causal
relationships between these attributes and their update
strategy. Finally, another aspect that will be addressed in the future is to
consider dynamic models where entities are created and deleted, as
 in~\cite{Giavitto2012}. 
%Finally, we are also working on more efficient
% translation towards timed automata to make possible the use of
% model-checking tools like UPPAAL \cite{uppaal} on more significant examples.
%Finally, it would certainly be interesting to find a systematic way for approximating stochastic rates into activities durations and decays.




%% 
%Related: reaction systems, petri nets with causal time and petri nets with timestamps
%

 \vspace{-0.2cm}
 \paragraph{\bf Acknowledgments.}
 This work was supported by the French project ANR BLANC 0307 01 - SYNBIOTIC. We thank M. Heiner and F. Pommereau for useful suggestions and discussions. 
%  
 \vspace{-0.4cm}
{\small
\bibliographystyle{abbrv}
\bibliography{biblio}
}

\newpage

\appendix
\input{appendix.tex}
\end{document}







\section{Repressilator}\label{app:repr}

Another example that is easily expressible with \andy is the
repressilator \cite{Elowitz}.  It is a synthetic genetic regulatory
network consisting of three genes connected in a feedback loop, such
that each gene inhibits the next gene and is inhibited by the previous
one. The repressilator exhibits a stable oscillation with fixed time
periods.
%%
We model it in \andy with three entities $\entities =\{s_1, s_2, s_3\}$
each with two levels representing an \emph{on}/\emph{off} state. Level
$1=on$ for all entities has decay time $\life_{s_i}(1)=1$; the set of
\potential activities is (no \obligatory activity are required):
%
\[
\begin{array}{c}
 r_1: \activ{\emptyset}{s_1}{1}{s_2}\\
 r_2: \activ{\emptyset}{s_2}{1}{s_3}\\
 r_3: \activ{\emptyset}{s_3}{1}{s_1}\\
\end{array}
\]
%
The SNAKES rendering of the repressilator is given in Figure~\ref{fig:repress}.

\begin{figure}
{\centering
\includegraphics[width=\textwidth]{repress.png}}
\caption{Petri net representation of the repressilator with Snakes}\label{fig:repress}
\end{figure}

Figure~\ref{fig:mgsB} shows the complete state graph where we identify
the characteristic oscillating behavior of the repressilator
(represented by cycles). However, notice that there are also paths
that leave the cycles to return into state $3$ where the 3 entities are
not expressed (level $0$). 

\begin{figure}[ht]
\begin{center}
\includegraphics[width=.5\textwidth]{B.pdf}
\end{center}
\caption{State graph of the repressilator}\label{fig:mgsB}
\end{figure}

In order to have a better understanding of these unexpected behaviors,
we use the MGS tool to generate the alternative state graph given
Figure~\ref{fig:mgsA} representing the time progression. In fact, in
this graph, each arc corresponds to a clock tick (phase
Ph.~\ref{item:clock}) followed by a composition of \potential
activities (phase Ph.~\ref{item:reaction}).
%%
The periodic behavior is clearly restricted to a subgraph (bold
cluster on Figure~\ref{fig:mgsA}); the other cluster (dashed on
Figure~\ref{fig:mgsA}) gathers the unexpected states.
%%
After analysing this graph, transitions going from the periodic
cluster to the other corresponds to evolutions with only time
progression and decay without any activity. It may be interpreted as
those cases that are unlikely to happen but still (at least in
principle) plausible which may explain the lack of robustness of such
a synthetic genetic regulatory network when  implemented in real scenarios.

\begin{figure}[ht]
\includegraphics[width=\textwidth]{A.pdf}
\caption{Time progression in the repressilator state space}\label{fig:mgsA}
\end{figure}

%% Moreover we have studied its state space with MGS obtaining a graph
%% that shows the periodic behavior typical of the repressilator. Figure
%% \ref{fig:mgsB} shows an extract of the complete state space where we
%% identify the oscillation (represented by cycles). In the complete
%% graph (Figure \ref{fig:mgsA}) notice that there are also paths that
%% leave the cycles. This corresponds to evolutions with only time
%% progression and decay without any activity and it may be interpreted
%% as those cases that are unlikely to happen but still (at least in
%% principle) plausible.  Thus the model is suitable to address
%% robustness matters as we can test the model against the appearance of
%% even the less likely to occur events.

%% \begin{figure}[ht]
%% \includegraphics[width=\textwidth]{B.pdf}
%% \caption{Extract of the state space of the repressilator}\label{fig:mgsB}
%% \end{figure}



\end{document}


CAMBIARE L DEGLI AUTOMI IN L CALLIGRAFICO SI CONFONDE CON GLI L DEI LIVELLI


COMMENTAIRE A CONSIDERER POUR UNE VERSION PLUS LONGUE



\comment{%
        Initialement on disait : ``chaque entité possède un ensemble
        d'attributs'', ce qui n'est pas le cas vu la formalisation. Si
        une entité possède un seul attribut, alors il vaut peut-être
        mieux parler de \emph{variable} ou d'\emph{observable} que
        d'entité (car on parle des variables ou des observables d'un
        système et qu'habituelement une entité/objet est caractérisé par
        plusieurs attributs): ``a measurable property of a physical
        system''. %
      }



\comment{%%
  Why restraining to decay? For instance, with this formalism,
  I cannot fill in a bathtub. 

  Using an arbitrary $d_\entity$ for the evolution of the state of
  $\entity$ subsumes both increase and decrease. Note also that it
  simplifies greatly the modeling of a \emph{clock}: it is enough to
  consider a $d_\entity$ with a limit cycle. Note that this does not
  prevent to check that $d_\entity$ is monotonic (that is, induce a
  strict order on $\setlev$ when $x \leq d_\entity(x)$ for all $x \in
  \setlev$) and to use this property in the tools (\eg to cut
  the state space).  %%
} %%



\comment{%%
  Again: we can have states that are not levels. It will extend at no
  cost the applicability of the formalism. The decreasing function on
  levels can be modeled by a map $d_\entity : \setlev \mapsto \setlev$. We can
  insists to have an infinite delay for the fixed points $x$ of $d_\entity :
  \life_\entity(x) = \omega \Leftrightarrow d_\entity(x) = x$ and that
  $\level{\entity}$ is a fixed point. 
  %% 
}



 \comment{%%
  The purpose/use of $v$ must be given here. %%
  To generalize decay, replace $v \in \mathbb{Z}$ by $d : \setlev_\entity
  \mapsto \setlev_\entity$ and the addition/subtraction by the
  application of $d$. Think to $d$ as the successor/predecessor
  function. Requiring $d$ \emph{injective} to have $d^{-1}$ is to strong
  because of the fixed points. What is the weakest relevant
  assumption?  %%
}


\comment{%%
  Why is the discharge not related to the duration of the call? How to
  model it?
        
  If the phone is plugged, it does not discharge when there is a phone
  call.  %%
} 
